home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Source Code / C / Applications / SML⁄NJ 93+ / Documentation / examples / prop.sml < prev    next >
Encoding:
Text File  |  1995-12-30  |  911 b   |  34 lines  |  [TEXT/R*ch]
  1. (* propositional calculus *)
  2.  
  3. datatype truth = TRUE | FALSE
  4.  
  5. datatype term
  6.   = VAR of string
  7.   | CON of truth
  8.   | NOT of term
  9.   | AND of term * term
  10.   | OR  of term * term
  11.  
  12. (* (~ p) and q  ==> AND(NOT(VAR "p"), VAR "q") *)
  13.  
  14. (* transform term to conjuctive normal form *)
  15.  
  16. fun negate (NOT(NOT p)) = negate p 
  17.   | negate (NOT p) = p (* BUG! *)
  18.   | negate (AND(p,q)) = OR(NOT p, NOT q)
  19.   | negate (OR(p,q)) = AND(NOT p, NOT q)
  20.   | negate p = NOT p
  21.  
  22. fun cnf (AND(p,q)) = AND(cnf p, cnf q)
  23.   | cnf (NOT(NOT p)) = cnf p
  24.   | cnf (NOT(AND(p,q))) = cnf(OR(negate p, negate q))
  25.   | cnf (NOT(OR(p,q))) = AND(cnf(NOT p), cnf(NOT q))
  26.   | cnf (OR(AND(p,q),r)) = AND(cnf(OR(p,r)),cnf(OR(q,r)))
  27.   | cnf (OR(p,AND(q,r))) = AND(cnf(OR(p,q)),cnf(OR(p,r)))
  28.   | cnf (OR(NOT p,q)) = cnf(OR(negate p, q))
  29.   | cnf (OR(p, NOT q)) = cnf(OR(p, negate q))
  30.   | cnf p = p
  31.  
  32. (* exercise: write a tautology checker.
  33.   (hint: use resolution) *)
  34.